COMMENT ⊗   VALID 00014 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00003 00002	SECTION 4. The Language of the Strategies
C00005 00003	4-I.  THE CHOICE STRATEGIES.
C00011 00004	4-II. EDITING STRATEGIES.
C00014 00005	4-III. COMBINING PRIMITIVE STRATEGIES.
C00015 00006	4-IV. THE AUTOMATIC STRATEGY SELECTION.
C00017 00007	SECTION 5. Theorem Proving Primitives.
C00022 00008	.REQUIRE "ANSWER.PUB" SOURCE_FILE
C00023 00009	APPENDIX.  The Syntax Equations for the Theorem Prover.
C00024 00010	A-I.  THE INPUT FORMAT
C00028 00011	
C00030 00012	A-II. THE SIMPLE STRATEGY LANGUAGE
C00032 00013	A-III.  THE COMMAND LANGUAGE
C00035 00014	A-IV. THE MATCHER
C00036 ENDMK
C⊗;
SECTION 4. The Language of the Strategies
.SKIP 3
.BEGIN DOUBLE SPACE
Frequently the user of a theorem prover "knows" a lot of detail
about the problem domain being axiomatized.  Much of this information
(almost by definiton) is domain-dependent and  thus doesn't fit the 
usual set of strategies as well as could be desired. Also much of this
information is heuristic in nature  and would be difficult to express
in the form of axioms.
To help with these problems we have introduced two new ideas: (1) a language
for describing strategies; and (2) new data types added to LISP
so that the user may tailor-make his own prover.

The strategy language allows Boolean expressions over properties
of clauses.  Major extensions of this idea are contemplated.

The programmable aspects allow the user to describe  first order statements, strategies
and pattern matching in an intuitive notation. With these facilities inside LISP
we can write new rules of inference and domain dependent theorem provers.

.NEXT PAGE
4-I.  THE CHOICE STRATEGIES.


Choice strategies occur in the following context: Given two  possible
candidates, C1 and C2, for the application of a binary rule of inference
I, a choice strategy will determine whether not we wish to form I(C1,C2).

Built-in choice strategies.

a) NONE  allows unrestricted applications of the rules of inference.

b) ANCESTRY implements the AFF strategy; that is, to apply I either C1 or
C2 must be an initial clauses, or, either C1 must appear in the derivation tree
of C2, or C2 must appear in the tree of C1.

c) SUPPORT designates the set-of-support strategy. This strategy basically says 
that every first-level deduction must have one of its parents in the
support set.  SUPPORT must be followed
by an argument list describing which  statements are to be supported.
The elements of the argument list may either be clause numbers or names
which the user has associated with certain input clauses.

Example: SUPPORT[1,2,AXIOM[2],THEOREM] would put clauses numbered 1 and 2, the 
clause AXIOM[2], and all clauses with name, THEOREM, in the support set.


d) VINE strategy says that either C1 or C2 must be an initial clause.  This 
strategy is known to be incomplete, but is useful in many cases. 

e) UNIT strategy says that either C1 or C2 are singletons(unit clauses).  Again, this strategy
is not complete, but is useful as a "quick-kill" or "end-game" strategy.
It is easy to show that if there is a UNIT-refutation then there is a VINE-form
refutation. It is also easy to show that if all the initial statements are either
units(singletons) or are of the form L1∧L2∧...∧Ln ⊃ M then there is a UNIT 
proof.


f) P1 is the P1-deduction of Robinson. Here it is required that either
C1 or C2 contain only positive literals. This strategy is complete.


g) MODEL is the implementation of a very simple  case of the model-relative 
deduction strategy of Luckham.  Model-relative deduction is a generalization
of P1 deduction and is complete.  Deduction relative to a model says
that at least one of the clauses C1 or C2 be false of the model.  MODEL expects 
an argument list describing a binary partition of the predicate letters appearing
in the initial clauses. In the current restricted implementation this says either C1
or C2 must have zero intersection with the two members of the partition.
For example, MODEL[;<all predicate letters occurring in problem>] is equivalent to
P1-deduction; MODEL[P,=;R] defines a partition with positive occurrences of P and
=, and negative occurrences of R.


h) DEFMODEL can be used to designate a LISP function to define a model for the
current set of statements.  DEFMODEL expects a single argument which is the name
of a LISP function(of one argument) and which implements the defining conditions
of a model. The use of this strategy requires knowledge of the representation
of clauses.

i) EQUALITY signals that the replacement rule, paramodulation, is to be used.
EQUALITY needs two arguments: a predicate name to be interpreted as equality;
and second, a number, called PDEPTH, which determines how deep in the nesting
of function symbols the matcher will look in attempting to match terms.
For example, a PDEPTH of 1 says only examine primary occurrences of terms.


.SKIP 3
4-II. EDITING STRATEGIES.
.SKIP 3


Editing strategies are applied to the results of the rules of inference.
These strategies are used to  filter out some of the deductions which a rule
of inference has generated.

Built-in editing strategies.

a) DEMOD is a rule of simplification most commonly used in conjunction with
EQUALITY. DEMOD takes two arguments. The first describes a list of equality units;
the second, a number named DDEPTH which,like PDEPTH, determines a bound on the
matching routines.


b) DEPTH takes a single integer argument interpreted to be a bound on the depth of
function symbol nesting which must not be exceeded if the deduction is to be retained.

For example, DEPTH[4].

c) LENGTH also takes an integer argument and gives a bound on the number of literals
which will be allowed in any deduction.

d) SELDEPTH takes function symbol-number pairs as arguments.  SELDEPTH is a refinement
of DEPTH in that the allowable depth of nesting of each function symbol is determined
by the corresponding number. 

e) Any of the primitive constructs of the pattern language: TREE, LENGTH, DEPTH, or
OCR.  For example if OCR[f(e,e)] were to appear in an editing strategy then any
clauses which contained "f(e,e)" would be rejected.

.SKIP 3
4-III. COMBINING PRIMITIVE STRATEGIES.
.SKIP 3
Boolean combinations of built-in or user-defined strategies are allowed.
For example, a reasonable choice strategy  is: ancestry filter form
with a set of support being the negation of the statement to be proved.
This can be written as:

 ANCESTRY ∧ SUPPORT[THM];


An editing strategy which filters out all clauses whose length (number of literals)
is greater than 4 or whose depth (depth of nesting of function symbols)
is greater than 3 can be expressed as:

LENGTH[4] ∨ DEPTH [3];

See the Appendix (A-II) for the rules of combination.

.SKIP 3

4-IV. THE AUTOMATIC STRATEGY SELECTION.
.SKIP 3
A very simple procedure is used to select the strategies in PROVE-mode.
The choice strategies are ANCESTRY and, if THM is present as an axiom name
, then SUPPORT[THM] is also used.  Also, if an equality predicate
letter is declared, then equality replacement with a depth bound of 4 is added.

The editing strategies are determined by the maximum lengths and depths which occur in the 
input clauses.  If equality is present then a simplification list consisting of all the
positive units is used.

The strategy settings are automatically changed if the program is terminated without
finding a proof.


.NEXT PAGE
SECTION 5. Theorem Proving Primitives.
.SKIP 3
It is now possible to write LISP-like programs which control the actions
of the theorem prover and manipulate clauses.  Data types  for CLAUSES,
STRATEGIES, and PATTERNS have been added to LISP so that the user can
describe his clause manipulations in the same notation which is used
to drive the on-line prover.  LISP functions, TRYTIL and FIND, have
been defined to perform controlled proof-attempts and clause-list searching.

1. Data Types.

a) [CLAUSES <clauses>] is used to introduce new clause lists to the program.
For example: (SETQ X [CLAUSES DSK:FOO])  when executed will assign to X the
clauselist manufactured from the statements on file FOO.

b) [CHOICE <strategy>] and [EDIT <strategy>] introduce the appropriate
strategies.

c) [PATTERN <pattern>] is useful in conjunction with FIND to filter out  clauses
which match <pattern>.


2. Procedures.

(TRYTIL <clauses><choice-strategy><edit-strategy><termination condition>)

.BEGIN VERBATIM

where:
1) <clauses> is a list of clauses .

2) <choice-strategy> is a representation of a choice strategy.

3) <edit-strategy> represents an editing strategy.

.END
4) <termination condition> is a functional argument which will be evaluated
periodically during the execution of the TRYTIL.  As long as the condition
evaluated to NIL the proof attempt will continue. If the condition becomes true
then TRYTIL will return the list of all deductions which have been made.

For example:

(TRYTIL [CLAUSES DSK: FOO] [CHOICE ANCESTRY∧SUPPORT[THM]]
[EDIT LENGTH[4]∨DEPTH[3]] (FUNCTION (LAMBDA()(GREATERP LEVEL 3))) )

will begin a proof search using file DSK:FOO with choice strategy being AFF and
supporting the negation of the theorem.  Deductions whose length is greater than
4 or whose depth of function nesting is greater than 3 will be discarded.
The proof search will terminate at the end of level 3.

If a refutation is discovered during any attempt, (QED) is returned. If no refutation
is found, then the on-line editor is called to give the user a chance to examine
the current proof environment. There is a third way to exit TRYTIL: since
the on-line editor is available inside the proof attempt, typing ABandon <clauses>
to the  editor will force termination of the proof attempt and will return the 
selected <clauses>.


(FIND <clauses><pattern>)

where: 
1) <clauses> is a list of clauses.
2) <pattern> is a condition which is to be applied to each element of <clauses>.

The value of FIND is a list of all elements of <clauses> which satisfy the
<pattern>.


.END

.NEXT PAGE
.REQUIRE "ANSWER.PUB" SOURCE_FILE
.NEXT PAGE

.BEGIN DOUBLE SPACE
APPENDIX.  The Syntax Equations for the Theorem Prover.


The parsers for the input syntax and the command language are both contstructed
by Lynn Quam's
Syntax Directed Input Output program.

.SKIP 1
.END

A-I.  THE INPUT FORMAT
.SKIP 1
.BEGIN DOUBLE SPACE
The usual form for input consists of the declarations of the non-logical
constituents of the axioms, followed by a sequence of statements.  The statements
may be assigned names, and if a statement whose name 
is the same as the current value of THEOREMNAME is present that statement
is negated before being added to the memory of the prover.
The  LISP atom THEOREMNAME is initialized to THM.
.END
.SKIP 2
.BEGIN VERBATIM
<INPUT>	::=<DECOP>:<OPLIST>;
	::=<ID>:
	::=<STATEMENT>

<DECOP>	::=VAR | INF_OP | INF_PRED | PRE_OP | PRE_PRED | EQUALITY

<OPLIST>::=<OP>,<OPLIST>
	::=<OP>

<STATEMENT>	::=;
	::=<S1>;

<S1>	::=<S2>
	::=<S1><EQUIV><S2>

<S2>	::=<S3>
	::=<S2><IMP><S3>

<S3>	::=<S4>
	::=<S3><OR><S4>

<S4>	::=<S5>
	::=<S4><AND><S5>

<S5>	::=(<S1>)
	::=<NOT><S5>
	::=<QFF><BODY>
	::=<PRED>

<BODY>	::= <IVAR><S5>
	::=(<VARLIST>)<S5>

<VARLIST>::=<IVAR>,<VARLIST>
	::=<IVAR>
.END

.BEGIN DOUBLE SPACE

In the following, the routines corresponding to <PREPREDLET>, <INFPREDLET>, <IVAR>, <PREFN>, and
<INFN> check the lists of prefix- and infix- predicate and function letters, and
the variable list, all of which were manufactured by the appropriate declarations.

.END

.BEGIN VERBATIM

<PRED>  ::=<PREPREDLET><ITMLST>
	::=<PREPREDLET>
	::=<TM><INFPREDLET><TM>

<ITMLST>::=(<ITMS>)

<ITMS>  ::=<TM>,<ITMS>
	::=<TM>

<TM>    ::=<IVAR>
	::=<PREFN><ITMLST>
	::=<PREFN>
	::=(<TM>)
	::=<TM><INFN><TM>


The logical connectives are defined as follows:

<EQUIV>	::= ≡ | ↔ 

<IMP>	::= ⊃

<OR>	::= ∨

<AND>	::= ∧

<NOT>	::= ¬

<QFF>	::= ∀ | ∃
.END

.NEXT PAGE
A-II. THE SIMPLE STRATEGY LANGUAGE
.BEGIN DOUBLE SPACE

The most straightforward application of the strategy language consists
of using Boolean combinations of the builtin strategies. 
.END
.BEGIN VERBATIM

<STRATEGY>::=<F1>;

<F1>	::=<F2>
	::=<F1><OR><F2>

<F2>	::=<F3>
        ::=<F2><AND><F3>

<F3>	::=(<F1>)
	::=<NOT><F3>
	::=<PREDIC>

<PREDIC>::=ANCESTRY
	::=NONE
	::=VINE
	::=UNIT
	::=P1
	::=SUPPORT[<C>]
	::=MODEL[<PREDLST>;<PREDLST>]
	::=EQUALITY[<OP>;<NUMBER>]
	::=DEMOD[<CLAUSES><NUMBER>]
	::=DEFMODEL[ID]
	::=LENGTH[<NUMBER>]
	::=DEPTH[<NUMBER>]
	::=SELDEPTH[<FNLST>]
	::=<MPRM>

<PREDLST>
	::=<ID>,<PREDLST>
	::=<ID>
	::=

<FNLST>	::= <FP>;<FNLST>
	::= <FP>

<FP>	::=<OP>,<NUMBER>

.END
.NEXT PAGE
A-III.  THE COMMAND LANGUAGE

.BEGIN VERBATIM



<CLAUSES> ::= <C>,<CLAUSES>
	::= <C>

<C>	::= @<STATEMENT>	<STATEMENT> is in A-I.
	::= DSK: <FILE>
	::= <NUMBER>
	::= <ID>[<VARLIST>]
	::= <ID>
	::= FIND [<ID>,<MATCH>]
	::= FINDC [<MATCH>]

<FILE>	::= <ID>
	::= (<ID>.<ID>)

<VARLIST> ::= <NUMBER>,<VARLIST>
	::= <NUMBER>

<COMMAND ::= AB <CLAUSES>;	ABandon proof attempt
	::= AB;
	::= AD <CLAUSES>;	ADd clauses to clauselist.

	::= AN <CLAUSES>;	display ANcestry

	::= CH;			CHange strategies
	::= CL <ID>;		CLear name from symbol table
	::= CO;			COntinue with proof search
	::= CU;			display CUrrent strategies

	::= DE <CLAUSES>;	DElete clauses
	::= DI <CLAUSES>;	DIsplay clauses
	::= DO <NUMBER>;	move DOwn
	::= DS <FILE>;		set output to DSk(see EOf)

	::= EO;			make End Of File
	::= EV;			enter Lisp's EVAL
				  (leave via @END)
	::= EX;			EXecute subproof with 
				   standard strategies.
	::= FD;			Float Down clause list
	::= FU;			Float Up clause list

	::= GO <NUMBER>;	GO to designated clause
	::= HA;			HAlt to prover
	::= HE;			type HElp message

	::= PA <CLAUSES>;CLAUSES>; PAramodulate selected 
				     clauses.
	::= PR <CLAUSES>;	Initialize subproof
				  (see US,EX,and TR.)
	::= RE <CLAUSES>;<CLAUSES>; REsolve clauses

	::= SE <ID> <CLAUSES>;	SEt id as name for clauses.
	::= SI <CLAUSES>; BY <CLAUSES>; SImplify
	::= SU <TM> FOR <TM> IN <CLAUSES>; SUbstitute.
					     (add to ASSERT)
	::= SY;			display current SYmbol table.

	::= TE <CLAUSES>;	TErminate; (see Sec. 2-IV).
	::= TE;
	::= TR;			TRies subproof with user's
				   strategies.

	::= UP <NUMBER>;	move UP  n clauses.

.END
.NEXT PAGE
A-IV. THE MATCHER

.BEGIN VERBATIM

<MATCH>	::= <M2>
	::=<MATCH> ∨ <M2>

<M2> 	::= <M3>
	::= <M2> ∧ <M3>

<M3> 	::= (<F1>)		<F1> in A-II.
	::=¬<M3>
	::=<MPRM>

<MPRM>	::= <ARG><MOP><ARG1>

	::= OCR[<PAT>]
	::=TREE[<CNAME>]

<MOP> 	::= =
	::= <
	::= >

<ARG1> ::= <ARG>

<ARG> 	::= LENGTH
	::=DEPTH
	::=<NUMBER>

<CNAME>	::= <NUMBER>
	::= <ID>[<VARLIST>]	<VARLIST> in A-III.
	::= <ID>

<PAT>	::= <NOT><PRED>		<PRED> in A-I.
	::=<PRED>
	::=<TM>			<TM> in A-I.
	::=<FNLET>

<FNLET> ::=<INFN>		<INFN> in A-I.
	::=<PREFN>		<PREFN> in A-I.
.END